FDL - Nuprl Lemma : sends-bound-property

Nuprl Lemma : sends-bound-property

E, X1, X2:Type, info:(E

(Id

X1+(IdLnk

E)

X2)), pred?:(E

(E+Unit)),

p:(

e:E, l:IdLnk.

p:(

e':E.

p:(

e'':E.

p:(rcv?(e'')

p:(

sender(e'') = e

p:(

link(e'') = l

p:(

e'' = e'

e'' < e' & loc(e') = destination(l)

Id), e:E, l:IdLnk.
{

e'':E.
{rcv?(e'')
{

sender(e'') = e
{

link(e'') = l
{

e'' = sends-bound(p;e;l)

e'' < sends-bound(p;e;l)
{

& loc(sends-bound(p;e;l)) = destination(l)

Id}

Definitions {T}, Unit, x:A. B(x), sends-bound(p;e;l), Prop, b, rcv?(e), sender(e), IdLnk, link(e), P Q, P & Q, P Q, e < e', Id, loc(e), t T, destination(l), x:A. B(x)

Lemmas ldst wf, loc wf, Id wf, cless wf, link wf, IdLnk wf, sender wf, rcv? wf, assert wf, unit wf